Tutorial for Alloy Analyzer 4.0を読む
この当時が一番盛り上がっていた時期なのだろうか
このページのUIが独特
この人Sidenote好きだね
Chapter 0
ミスってるモデルを書いて徐々に改善する
The goal of a writing a model is to describe some aspect of a system (but not the entire system), constrain it to exclude ill-formed examples, and check properties about it.
システムのある側面を記述し、反例を削ぎ落とす
起こりうる問題
モデルの定義がおかしい
e.g. 過度な制約、過小な制約
モデル化する対象がおかしい
探索するスコープを限定してチェックを行う
(スコープ内では)健全だが、(スコープ外をチェックできないので)完全でない
ここで言ってるdeclarativeって「propertyを記述すること」を言ってるのかなmrsekut.icon
Chapter 1
File Systemを題材に1から6まである
File System Lesson I
Alloyを読み解く3つの抽象化レベル
(上に行くほど高い抽象化)
OOP
集合
atom, relation
例として以下のようなAlloyコードを3つの抽象化レベルで解釈できるということ
code:alloy
sig S extends E {
F: one T
}
fact {
all s:S | s.F in T
}
最も低い抽象化レベルであるatom, relationsで解釈するほうが厳密性が高い
けど、OOPっぽく解釈することもできるよ、ぐらいの意味合い
数学に慣れているなら集合的に解釈するのがちょうど良さそうmrsekut.icon
OOPパラダイムに縛られないし、
atom, relationsは具体的すぎるだろう
これなんでFSObject表示されるんだろうねmrsekut.icon
https://gyazo.com/9dd31c2c8a08b900d3d455d66a2b0cf3
Alloy 6かなにかに上がったタイミングでデフォルトで表示する項目が変わったのかな
Alloy 3の本を読んでるときにも思った
File System Lesson I Walkthrough
File System Lesson II
ファイルの移動や削除など、動的な性質についても見ていく
FileSystemという統括する用のsigがある
factで~e使うんじゃなくてpropertyのところで使うのとは違うんだろうか code:alloy(diff)
sig FileSystem {
...
contents: Dir lone-> FSObject,
- parent: FSObject ->lone Dir
+ parent: ~contents
}{
File System Lesson III
正しいと思って書いたが、インスタンスを見てみてみるとちょっと違う、と気づいたときに、式を正しく解釈して修正するの、いくらかの能力が必要そうmrsekut.icon
live in root.*contents
「全てのliveが」とは言ってない
File System Lesson IV
書き方をブラッシュアップして簡潔な記述に変えていく
code:diff
sig FileSystem {
- root: Dir,
+ root: Dir & live,
live: set FSObject,
- contents: Dir lone-> FSObject,
+ contents: Dir -> FSObject,
- parent: FSObject ->lone Dir
+ parent: (live - root) ->one (Dir & live),
}{
- no root.parent
live = root.*contents
- contents in live->live
parent = ~contents
}
factのところでparent = ~contentsするなら、
そもそもcontents: ~parentとしても良い気がするがmrsekut.icon
2つの定義を比較してinstanceに差があるものを表示する、とかやりたいなmrsekut.icon
「この改善によって、このinstanceが除外された」というのを確認したい
2つのモデルを同時に書いて、AのinstanceでBの制約を満たさないもの、という条件を書けばいいのか
File System Lesson V
動的なものを見ていく
Alloyの関数はtrue/falseにしか評価しない
inputとoutputを両方関数に渡す
実引数の組み合わせが有効であればtrueを返す
引数に'を使ってるけど、Alloy6では使えなさそうmrsekut.icon
このmove predの解釈
code:alloy
(x + d) in fs.live
fs2.parent = fs.parent - x->(x.(fs.parent)) + x->d
}
他の言語のように解釈するなら、
元の状態fsで、xをdに移動した後の状態fs2を返す
のように考えられる
実際は、前状態のfs、後状態のfs2があり、
そのfs2が「fs上でxをdに移動したもの」になっているときにtrueを返す
(x + d) in fs.live
xもdも元のfsに含まれている
fs2.parent = (fs.parent) - (x->(x.(fs.parent))) + (x->d)
fs.parent ..: 前の状態のfsから
- (x->(x.(fs.parent)): xからxの古い親へのマッピングを取り除き
+ (x->d): xの新しい親へのマッピングを追加したもの
fs2.parent = : がfs2.parentを形成したものである
関係を演算する、というのが慣れるまでは難しそうmrsekut.icon
https://gyazo.com/ed0915e272bed0a5a83dcaf9d01b1d0a
読み方がわからん
これでxをdにmoveしてると
|って、let..inのin的な意味でも使えるんだ
code:alloy
let subtree = x.*(fs.contents) |
fs2.parent = fs.parent - subtree->(subtree.(fs.parent))
assertionを書くが反例が見つかる
File System Lesson VI
Vの反例を直す
説明の意味はわかるが、この図の->が何なのかわからない
遷移したというのはわかるが、visualizer上のなんなのか
visualizer上でどのようにこれを確認できるのかがわからない
https://gyazo.com/b1b46a8dce409a3c4a05bf57124b7be0
要するに、
操作後のcontenstsが空でない場合は、当然、操作前のrootとおなじになるが、
もし、操作後のcontentsが空になると、(制約が甘いので)rootが任意に変更される可能性がある
the rows of the parent relation in the post-state to be a subset of the rows in the pre-state.
ある関係{(a,b),(c,d)}のようなものがある時、(a,b)は1つのrowである
コード中のfs2.parent = fs.parent - x->(x.(fs.parent)) + x->dの部分で
fs2.parentが、fs.parentのサブセットになっていることを言っている
Chapter 2 examines a more advanced Alloy model which solves the famous River Crossing planning problem, using the util/ordering module for modeling ordered state.